%\newcommand{\sx}[1]{$\langle\mbox{#1}\rangle$}
\newcommand{\sx}[1]{\mbox{\underline{\em #1}}$\;$}
\newcommand{\lx}[1]{$\mbox{\tt\bf #1}\;$}
\newcommand{\kw}[1]{$\mbox{\tt\bf #1}\;$}
\newcommand{\myor}{$\;\;|\;\;$}
\newcommand{\is}{$\longrightarrow$}
\renewcommand{\arraystretch}{1.2}
\newcommand{\option}[1]{
\mbox{$\;[$}#1\mbox{$]\;$}
}
\newcommand{\pstar}[1]{
\mbox{$\;\{$}#1\mbox{$\;\}^*$}
}
\newcommand{\pplus}[1]{
\mbox{$\;\{$}#1\mbox{$\;\}^+$}
}

\newcommand{\sxtitle}[1]{
\multicolumn{3}{l}{\bf #1}\\
}
\newcommand{\sxcomment}[1]{
\multicolumn{3}{p{\textwidth}}{#1}\\
}

\begin{syntax}
\sxtitle{Package:}
\sxcomment{
A Lustre package is a sequence (semantically a set) of declarations of constants, types,
functions or nodes. 
}
\sx{LusPack} & \is & \pstar{\sx{OneDecl}}\\
\sx{OneDecl} & \is & \sx{ConstDecl} \myor \sx{TypeDecl} \myor \sx{FuncDecl} \myor
\sx{NodeDecl} \\
\\
\sxtitle{Constant Declarations:}
\sxcomment{A constant can be declared with its type and/or value. If no value
is given, the constant is considered as imported.
Imported constants of a same type can be given as a list.
The type of defined constant can be given for more precision.}

\sx{ConstDecl} & \is & \kw{const} \pplus{\sx{OneConstDecl}} \lx{;} \\

\sx{OneConstDecl} & \is & \pstar{\sx{Idf} \lx{,}} \sx{Idf} \lx{:} \sx{Type}\\
                  & \myor & \sx{Idf} \lx{=} \sx{Exp} \option{\lx{:} \sx{Type}} \\
\\
\sxtitle{Type Declarations:}
\sxcomment{A declared type can be external (just a name) or declared.
Declared types are either aliases on type expressions, or built types
(structured or enumerated).}
\sx{TypeDecl} & \is & \kw{type} \pplus{\sx{OneTypeDecl} \lx{;}}\\
\sx{OneTypeDecl} & \is & \pstar{\sx{Idf} \lx{,}} \sx{Idf} 
                    \myor \sx{Idf} \lx{=} \sx{Type}\\
                    & \myor & \sx{Idf} \lx{=} \sx{TypeBuilder} \\
\sx{TypeBuilder} & \is & \kw{enum} \lx{\{} \pstar{\sx{Idf} \lx{,}} \sx{Idf} \lx{\}} \\ 
         & \myor & \kw{struct} \lx{\{} \pstar{\sx{Fields} \lx{;}} \sx{Fields} \lx{\}}\\
\sx{Fields} & \is & \pstar{\sx{Idf} \lx{,}} \sx{Idf} \lx{:} \sx{Type} \\
\\
\sxtitle{Type Expression:}
\sxcomment{Those expressions are used to specify the type of a variable, a field, etc.
We also talk about {\em immediate} type, to outline the difference with {\em built types}.
Immediate types are predefined types, type identifiers (references to declared types)
or static arrays.}

\sx{Type}  & \is & \sx{PredefType} \myor
			\sx{Idf} \myor \sx{Type} \lx{\^{ }} \sx{Exp}\\
\\
\sx{PredefType} & \is & \kw{bool} \myor \kw{int} \myor \kw{real}\\
\end{syntax}

\begin{syntax}
\sxtitle{Function  Declarations:}
\sxcomment{A function is declared with the names and types of its formal
parameters.}
\sx{FuncDecl}  & \is & \kw{function} \sx{Idf} 
                \lx{(} \sx{VarDeclList} \lx{)}
               \kw{returns}
                \lx{(} \sx{VarDeclList} \lx{)}\\
\\
\sx{VarDeclList} & \is &  \pstar{\sx{VarDecl} \lx{;}} \sx{VarDecl} \\
\\
\sx{VarDecl} & \is & \pstar{\sx{Idf} \lx{,}} \sx{Idf} \lx{:} \sx{Type} \\
\\
\end{syntax}
\begin{syntax}

\sxtitle{Node  Declaration:}
\sxcomment{A node can be declared with a complete
description of its dynamic behaviour, or by implicitely
reusing the dynamic behaviour of another node.
A node can have static parameters (we also talk about {\em template node},
or no (in which case we also talk about {\em actual node}).}

\sx{NodeDecl} & \is &
\kw{node} \sx{Idf} \option{\sx{StaticProto}} \sx{NodeProto} \sx{NodeBody} \\
& \myor &
\kw{node} \sx{Idf} \option{\sx{StaticProto}} \lx{=}
\sx{Idf} \option{\sx{StaticArgList}} \lx{;} \\
\\
\sxcomment{Static parameters are constants and abstract types,
or nodes.}
\sx{StaticProto} & \is &
{\bf \verb'<<'} \pstar{\sx{StaticParam} \lx{;}} \sx{StaticParam} {\bf \verb'>>'}
\\
\sx{StaticParam} & \is & \kw{type} \sx{Idf}
                       \myor
								\kw{const} \sx{Idf} \lx{:} \sx{Type} \\
	& \myor & \kw{node} \sx{Idf} \sx{NodeProto}\\
\\
\sxcomment{A node prototype defines the formal inputs/outputs 
of a node (in some sence the "type" of the node).
Formal node parameters are typed identifiers with an optionnal 
formal clock).}

\sx{NodeProto} & \is & \lx{(} \sx{ClockedVarDeclList} \lx{)}
\lx{returns} \lx{(} \sx{ClockedVarDeclList} \lx{)}\\
\\
\sx{ClockedVarDeclList}& \is & \pstar{\sx{ClockedVarDecl} \lx{;}} \sx{ClockedVarDecl}\\

\sx{ClockedVarDecl} & \is & 
	\sx{VarDecl} \kw{when} \sx{Idf}
	\myor
	\lx{(} \sx{VarDeclList} \lx{)} \kw{when} \sx{Idf} \\
\\
\sxtitle{Node Body:}
\sxcomment{It contains an optionnal set of local variable definitions and 
a sequence (semantically a set) of equations.}
\sx{NodeBody} & \is & \option{\kw{var} \sx{ClockedVarDeclList} \lx{;}} 
	\kw{let} \pplus{\sx{Equation} \lx{;}} \kw{tel}
\\
\sxcomment{An equation is either an assertion or a "real" equation.}
\sx{Equation} & \is & \kw{assert} \sx{Exp} \myor \sx{LeftPart} \lx{=} \sx{Exp}\\

\sxcomment{A left part is a non-empty list of left item.
A left item denotes a variable "piece": a full variable, the field of a structured
left item, an element or a slice of an array left item.}

\sx{LeftPart} & \is & 
\option{\lx{(}} \pstar{\sx{LeftItem} \lx{,}} \sx{LeftItem} \option{{\lx)}} \\
\\
\sx{LeftItem} & \is & \sx{Idf} \myor  \sx{LeftItem} \lx{.} \sx{Idf}
\myor \sx{LeftItem} \lx{[} \sx{Exp} \lx{]}\\
& \myor & \sx{LeftItem} \lx{[} \sx{Exp} \lx{..} \sx{Exp}
\option{\kw{step} \sx{Exp}} \lx{]}\\
\end{syntax}
\begin{syntax}

\sxtitle{Expressions:}
\sx{Exp}
   & \is & \sx{PredefConst} \myor \sx{Idf} 
			\myor  \sx{UnOp} \sx{Exp} \myor \sx{Exp} \sx{BinOp} \sx{Exp}\\
	& \myor &  \kw{if} \sx{Exp} \kw{then} \sx{Exp} \kw{else} \sx{Exp}
			\myor \kw{with} \sx{Exp} \kw{then} \sx{Exp} \kw{else} \sx{Exp}\\
	& \myor & \sx{Exp}.\sx{Idf} \myor \sx{Exp}\lx{[}\sx{Exp}\lx{]}
			\myor \sx{Exp}\lx{[}\sx{Exp}\lx{..}\sx{Exp}\option{\kw{step}\sx{Exp}}\lx{]}\\
	& \myor & \sx{NaryOp}\lx{(}\pstar{\sx{Exp}\lx{,}}\sx{Exp}\lx{)} \\
	& \myor & \lx{(} \pstar{\sx{Exp} \lx{,}} \sx{Exp} \lx{)} \\
   & \myor & \sx{Idf} \lx{\{} 
					\pstar{\sx{Idf} = \sx{Exp} \lx{;}} \sx{Idf} = \sx{Exp} \lx{\}}\\
	& \myor & \sx{NodeExpression}
					\lx{(} \pstar{\sx{Exp} \lx{,}} \sx{Exp} \lx{)}\\
\\
\sxcomment{Integer and floating point notations are following the ansi-c syntax.}
\sx{PredefConst} & \is & \sx{Integer} \myor \sx{Real} \myor \kw{true} \myor \kw{false}\\
\\
\sxtitle{Operator denotations:}
\sxcomment{The effective node construction denotes an actual operation
wich can be a predifined operation, or a user defined operation,
in which case a list of effective static parameters can be given.}
\sx{NodeExpression} & \is & \kw{operator} \sx{PredefOp} \\
                   & \myor & \sx{Idf} \option{\sx{StaticArgList}}\\
\sxcomment{The keyword \kw{if} is denoting the ternary operation
\kw{if}...\kw{then}...\kw{else}...}
\sx{PredefOp} & \is & \sx{Unop} \myor \sx{BinOp} \myor \kw{if} \\
\\
\sx{Unop} & \is & \kw{not} \myor \lx{-} \myor \kw{pre} \myor \kw{current}\\
\\
\sx{BinOp} & \is &
{\bf \verb'->'} \myor \kw{when} \myor \kw{or} \myor \kw{xor} \myor \kw{and} 
            \myor {\bf \verb'=>'} \myor \lx{=} \myor {\bf \verb'<>'} 
\myor {\bf \verb'<'} \myor {\bf \verb'>'} \\
& \myor & {\bf \verb'<='} \myor {\bf \verb'>='}
\myor \lx{+} \myor \lx{-}
\myor \lx{*} \myor \lx{/} \myor \kw{div} \myor \kw{mod} \myor 
{\bf \verb'^'} \myor {\bf \verb'|'}\\
\\
\sx{NaryOp} & \is & {\bf \verb'#'} \myor \kw{nor}\\
\\
\sxtitle{Static arguments:}
\sxcomment{The strict way is to specify the nature (const, type or node)
of a effective static; however, the nature can be 
avoided when the parameter is:
a {\bf simple} arithmetic and logic expression (typically {\tt n-1}),
a predifined type or constant (or an array of),
a predifined operator,
or even a single identifier (in this case, the compiler will try to
compute the nature according to its naming environment).}

\sx{StaticArgList} & \is &  
{\bf \verb'<<'} \pstar{\sx{StaticArg} \lx{,}} \sx{StaticArg} {\bf \verb'>>'}\\
\sx{StaticArg} & \is & 
	\kw{type} \sx{Type} \myor \kw{const} \sx{Exp} \myor 
	\kw{node} \sx{NodeExpression}\\
	& \myor & \sx{PredefType}\pstar{\lx{\^{}} \sx{Expression}}
	  \myor   \sx{PredefConst}\pstar{\lx{\^{}} \sx{Expression}} \\
	& \myor & \sx{SimpleExpression} \myor \kw{operator} \sx{PredefOp} \myor \sx{idf}

\end{syntax}

\end{document}  


